w:World. FairFifo  (e:E. loc(e) ~ loc(e)) 

latex

Definitions

destination(l), <a,b>, Id, s = t, P  Q, False, A, AB, , {x:A| B(x) }, , tag(k), lnk(k), act(k), islocal(k), kindcase(k; a.f(a); l,t.g(l;t) ), x:AB(x), left+right, Knd, t  T, True, x:A. B(x), x:AB(x), b, Action(dec), Action(i), a(i;t), kind(a), act(e), ecase1(e;info;i.f(i);l,e'.g(l;e')), loc(e), kind(e), loc(e), w-info(w;e), isnull(a), E, World, FairFifo, {T}, SQType(T), s ~ t, P  Q, P & Q, P  Q, isrcv(k), isrcv(l;a), locl(a), rcv(l,tg), A & B

Lemmas

assert wf, w-isrcvl wf, assert-eq-lnk, Id sq, w-E wf, fair-fifo wf, world wf, w-a wf, w-action wf, true wf, not wf, false wf